package model.cnf;


import java.io.BufferedReader;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.List;
import java.util.Scanner;

/**
 * <p>
 * A implementation of {@link CNF} that store everything in memory.
 * </p>
 * <p>
 * Represent a CNF that is store in memory. Be aware that some CNF can be really big so MemoryCNF
 * will take even memory to be store, so only use them when you need to do a lot of I/O operation on
 * it unless use FileCNF for a minimal use of memory.
 * </p>
 */
public class MemoryCNF extends CNF {

	protected List<Clause>	clauses	= new ArrayList<Clause>();

	/**
	 * Create a memoryCNF.
	 * 
	 * @param CNFfile
	 *            the file of the cnf.
	 * @throws Exception
	 *             if there is a problem.
	 */
	public MemoryCNF(String CNFfile) throws Exception {
		this.CNFfile = new File(CNFfile);

		check();
	}

	/**
	 * Get all the data from the CNF file and store them in memory.
	 * 
	 * @throws Exception.
	 */
	private void putInMemory() throws IOException {
		clauses = new ArrayList<Clause>();

		BufferedReader br = null;
		try
		{
			InputStream in = new FileInputStream(CNFfile);

			InputStreamReader ipsr = new InputStreamReader(in);
			br = new BufferedReader(ipsr);

			String line;
			while ((line = br.readLine()) != null)
			{// lit la CNF
				int i;
				// System.out.println("lit une ligne");
				if (line.charAt(0) == COMMENTAIRE)
					continue;
				if (line.charAt(0) == DESCRIPTION)
				{
					Scanner sc = new Scanner(line.substring(SIZE_DESCRIPTION));
					declaredNumVar = sc.nextInt();
					declaredNumClause = sc.nextInt();
					continue;
				}

				List<Literal> c = new ArrayList<Literal>();
				Scanner sc = new Scanner(line);
				while ((i = sc.nextInt()) != 0)
					c.add(new Literal(i));

				addClause(c);
			}
		} catch (IOException e)
		{
			e.printStackTrace();
			throw e;
		}
		finally
		{
			if (br != null)
				br.close();
		}
	}

	@Override
	public String toString() {
		StringBuffer s = new StringBuffer();
		s.append("p cnf ");
		s.append(String.valueOf(declaredNumVar));
		s.append(" ");
		s.append(String.valueOf(declaredNumClause));
		s.append("\n");
		for (Clause cl : clauses)
		{
			s.append(cl.toString());
			s.append("0\n");
		}
		return s.toString();
	}

	@Override
	public File export(String cnf, File directory) {
		File res = new File(directory, cnf);
		FileWriter fw = null;

		try
		{
			res.createNewFile();

			fw = new FileWriter(res);
			fw.write(toString());

		} catch (IOException e)
		{
			e.printStackTrace();

			res.delete();
			res = null;
		}
		finally
		{
			try
			{
				if (fw != null)
					fw.close();
			} catch (IOException e)
			{
				e.printStackTrace();
			}
		}

		if (res != null)
			modify = false;

		lastExportFile = res;
		return res;
	}

	@Override
	public File export(File directory) {
		String name;
		try
		{
			System.out.println("prefix " + PREFIX + getFileName() + " suffix " + SUFFIX);
			name = File.createTempFile(PREFIX + getFileName(), SUFFIX, directory).getName();
		} catch (IOException e)
		{
			e.printStackTrace();

			return null;
		}
		return export(name, directory);
	}

	@Override
	public int size() {
		return clauses.size();
	}

	@Override
	public void check() throws IOException {
		putInMemory();

		stat = new Stat(this);

		modify = false;
	}

	@Override
	public List<Clause> getClauses() {
		return clauses;
	}

	@Override
	public void addClause(List<Literal> cl) {
		if (cl.isEmpty())
			return;

		modify = true;
		clauses.add(new Clause(cl));
	}

	@Override
	public void addClause(Clause cl) {
		modify = true;
		clauses.add(cl);
	}

	@Override
	public Clause getClause(int i) {
		return clauses.get(i);
	}

	@Override
	public void checkStat() throws IOException {
		stat = new Stat(this);
	}

	@Override
	public boolean close() {
		if (modify)
			if (export(CNFfile.getName(), CNFfile.getParentFile()) == null)
				return false;
		return true;
	}

	@Override
	public void closeWithoutExport() {
	}

}
